$\forall$$T$, $V$:Type, $A$, $B$:($T$$\rightarrow\mathbb{B}$), $f$:(\{$x$:$T$$\mid$ $\uparrow$($A$($x$))\} $\rightarrow$$V$), $g$:(\{$x$:$T$$\mid$ $\uparrow$($B$($x$))\} $\rightarrow$$V$).
\\[0ex]($\lambda$$x$.if $A$($x$) then $f$($x$) else $g$($x$) fi )
\\[0ex]=
\\[0ex][$\lambda$$x$.$\uparrow$($A$($x$))? $f$ : $g$]
\\[0ex]$\in$ \{$x$:$T$$\mid$ ($\uparrow$($A$($x$))) $\vee$ ($\uparrow$($B$($x$)))\} $\rightarrow$$V$